The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^1)).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

a(a(b(b(x1)))) → b(b(b(a(a(a(x1))))))
a(c(x1)) → c(a(x1))
b(c(x1)) → c(b(x1))

Rewrite Strategy: INNERMOST

(1) CpxTrsMatchBoundsProof (EQUIVALENT transformation)

A linear upper bound on the runtime complexity of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 1.
The certificate found is represented by the following graph.

Start state: 811
Accept states: [812, 813]
Transitions:
811→812[a_1|0]
811→813[b_1|0]
811→811[c_1|0]
811→814[a_1|1]
811→815[b_1|1]
814→812[c_1|1]
814→814[c_1|1]
815→813[c_1|1]
815→815[c_1|1]

(2) BOUNDS(O(1), O(n^1))